package karpiel.boguchwal.wojciech.przemek

import org.scalatest.FunSuite

class LauncherTest extends FunSuite {

  test("testMain") {
    Launcher.main(Array("--xD", "-f", "example.prmk"))
  }
  test("EH") {
    Launcher.main(Array("--xD", "-f", "Eckmann-Hilton.prmk"))
  }
  test("Catch invalid subtleties") {
    assertThrows[PrzemekException](
      Launcher.main(Array("--xD",
        """(set reverse
          |     (Pi (x Bool)
          |         (Pi (y Bool)
          |             (Pi (p (Id x y))
          |                 (Id y x))))
          |     (J
          |      ;;typFunc
          |      (lambda (x Bool)
          |        (lambda (y Bool)
          |          (lambda (p (Id x y))
          |            (Id y x))))
          |      ;;reflFunc
          |      (lambda (x Bool) (refl x))))
          |
          |
          |(set p-inv-eq-p
          |     (Pi (x Bool) (Pi (y Bool) (Pi (p (Id x y))
          |                                   (Id (((reverse x) y) p) p))))
          |     (J (lambda (x Bool) (lambda (y Bool) (lambda (p (Id x y))
          |                                  (Id (((reverse x) y) p) p))))
          |        (lambda (x Bool) (refl (refl x)))))
          |
          |tt
          |""".stripMargin)))
  }
}
